課程資訊
課程名稱
 正規方法
Formal Methods 
開課學期
 100-1 
授課對象
 電機資訊學院  電子工程學研究所  
授課教師
 王 凡 
課號
 EE5122 
課程識別碼
 921 U7600 
班次
  
學分
 3 
全/半年
 半年 
必/選修
 選修 
上課時間
 星期三2,3,4(9:10~12:10) 
上課地點
 博理103 
備註
 總人數上限：30人 
  
課程簡介影片
 
核心能力關聯
 核心能力與課程規劃關聯圖
課程大綱
為確保您我的權利,請尊重智慧財產權及不得非法影印
課程概述

I. 介紹
第一章 介紹 一週
II. 基礎理論
第二章 邏輯二週
第三章 狀態轉換系統 二週 包含部份作業以及簡單模型的建立
III. 正規方法
第四章 時態邏輯與模型檢驗 一週
第五章 定理證明與程式驗證 一週
第六章 處理代數 一週
第七章 嵌入式系統 (時間自動機、混和式自動機) 一週
第八章 VDM、Z、B、SDL 一週
第九章 UML與State Chart 一週
IV. 應用、案例、與工具
第十章 HOL/PVS 一週
第十一章 RED 與 Uppall(含實例解說) 一週
第十二章 CUDD/SMV/NuSMV 一週
第十三章 Statemate Rapsody 一週
 

課程目標
 本門課程再教導學生，在自動提升系統設計品質的基本理論與技術。簡單來說，就是讓學生瞭解、熟習複雜系統的除錯、測試、與驗證的自動化技術。
為什麼要修習這們課呢？目前大型計畫的研發成本，有50％已經都分配到驗證項目上。在有些IC設計公司，設置有高達70％的系統開發成本，都花在自動驗證項目上。但是，目前在工業界，仍然沒有一個令人滿意的驗證解決方案。IC設計公司、軟體公司、網路系統公司都仍然努力、絕望的控制驗證項目的成本。換句話說，我們可以設計初各種超炫的SOC、通訊程序、應用軟體、或手機。但是這些超炫的系統就是當機，被顧客退貨，還被罵到臭頭。根據歐美各大公司的經驗，要能發展高階系統，維持公司競爭優勢的主要關鍵技術，就是自動化驗證，以期能控制那50％以上的驗證項目成本。現在，系統設計、撰寫程式、製作通訊程序的成本，只佔系統開發成本20％以下。沒有令人滿意的驗證解決方案，我們只能無助的坐看其成本繼續攀升，打敗公司的競爭力。台灣公司與學生的缺點，在於短視近利，只想趕快把產品包裝賣出。對於紮根的驗證自動化技術，不是缺乏投資，就是完全無知。本門課程的目的，再讓學生瞭解、熟習，未來致勝技術，也就是自動驗證，的相關理論與技術，以提升台灣工業在未來的競爭力。
 
課程要求
 成績評量方式:期中考30% +期末考30%+實習40% 
預期每週課後學習時數
  
Office Hours
  
指定閱讀
  
參考書目
  
評量方式
(僅供參考)
    
課程進度
週次
日期
單元主題
無資料